Nuprl Lemma : divides_iff_div_exact
2,24
postcript
pdf
a
:
,
n
:
.
n
|
a
(
a
n
)
n
=
a
latex
Definitions
P
Q
,
P
&
Q
,
P
Q
,
P
Q
,
b
|
a
,
Prop
,
x
:
A
.
B
(
x
)
,
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
div
rem
sum
,
add
mono
wrt
eq
,
divides
iff
rem
zero
,
int
nzero
wf
,
divide
wfa
,
divides
wf
origin
a:
, n:
. n | a 
(a 
n)
n = a a:, n:. n | a (a n)n = a Q
Q Qx:A. B(x)
T
x:A. B(x)